﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

using SimpleIR;
using PInfoModel;

namespace PIPostAnalysis.UserQuery
{
	/// <summary>
	/// Represents information that a developer may be interested in wrt. a single method parameter.
	/// Includes static variables and the implicit "reciver parameter".
	/// Includes info for use during computation as well as query.
	/// </summary>
	public class SingleParamInfo
	{
		public static IRProgram PProg;
		public static CompleteAnalysisInfoForProgram CPInfo;
		public static CompleteAnalysisInfoMethodContext CPInfoCTX;

		/// <summary>
		/// The name of the parameter that this is the info for.
		/// </summary>
		public readonly IRRootIdentifier ParameterName;

		/// <summary>
		/// Set of all memory locations that are reachable from the memory location at some line in the method.
		/// </summary>
		public readonly HashSet<MemLocID> ReachableLocsAtSomePoint;

		/// <summary>
		/// Set of all locations where some value from the reachable at entry set is used.
		/// </summary>
		public readonly HashSet<Tuple<IRType, MemLocWPath, IRSourceLocation>> UsedLocations;

		/// <summary>
		/// Set of all locations where some value from the reachable at entry set is modified.
		/// </summary>
		public readonly HashSet<Tuple<IRType, MemLocWPath, IRSourceLocation>> ModLocations;

		public SingleParamInfo(IRRootIdentifier pname)
		{
			this.ParameterName = pname;
			this.ReachableLocsAtSomePoint = new HashSet<MemLocID>();
		
			this.UsedLocations = new HashSet<Tuple<IRType, MemLocWPath,IRSourceLocation>>();
			this.ModLocations = new HashSet<Tuple<IRType, MemLocWPath,IRSourceLocation>>();
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder(this.ParameterName.RootNameString() + "\n");

			HashSet<Tuple<string, int>> usedlocs = new HashSet<Tuple<string, int>>(this.UsedLocations.Select((Tuple<IRType, MemLocWPath, IRSourceLocation> slp) => new Tuple<string, int>(slp.Item3.FileName, slp.Item3.Line)));
			List<Tuple<string, int>> ull = new List<Tuple<string, int>>(usedlocs);
			ull.Sort();

			HashSet<Tuple<string, int>> modlocs = new HashSet<Tuple<string, int>>(this.ModLocations.Select((Tuple<IRType, MemLocWPath, IRSourceLocation> slp) => new Tuple<string, int>(slp.Item3.FileName, slp.Item3.Line)));
			List<Tuple<string, int>> mll = new List<Tuple<string, int>>(modlocs);
			mll.Sort();

			sb.Append("\tUsedLines={");
			for(int i = 0; i < ull.Count; ++i)
			{
				if(i != 0)
					sb.Append(", ");
				sb.Append(System.IO.Path.GetFileName(ull[i].Item1) + " line: " + ull[i].Item2.ToString());
			}
			sb.Append("}\n");

			sb.Append("\tModLines={");
			for(int i = 0; i < mll.Count; ++i)
			{
				if(i != 0)
					sb.Append(", ");
				sb.Append(System.IO.Path.GetFileName(mll[i].Item1) + " line: " + mll[i].Item2.ToString());
			}
			sb.Append("}\n");

			return sb.ToString();
		}

		private void MarkAllUses(PIMNode nn, IRBasicAccessPath basep, IRSourceLocation sl)
		{
			HashSet<MemLocID> mlids = PIModel.LocationIDSForNode(nn);
			foreach(MemLocID ll in mlids)
			{
				if(!this.ReachableLocsAtSomePoint.Contains(ll))
					continue;

				IRType loctype = nn.LocationType;

				if(loctype is IRNumericType || loctype is IREnumType || loctype is IRPtrType || loctype is IRReferenceType)
					this.UsedLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, basep), sl));
				else
				{
					if(basep.IsEmptyAccessPath)
					{
						foreach(IRBasicAccessPath pp in loctype.TypeDescription.AllTerminalAccessPaths)
							this.UsedLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, pp), sl));
					}
					else
					{
						IRType loadtype = basep.PathLast.FieldType;
						if(loadtype is IRNumericType || loadtype is IREnumType || loadtype is IRPtrType || loadtype is IRReferenceType)
							this.UsedLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, basep), sl));
						else
						{
							foreach(IRBasicAccessPath pp in loctype.TypeDescription.AllTerminalAccessPaths)
							{
								IRBasicAccessPath wp = PProg.GetAccessPathExtensionPost_WPath(basep, pp);
								this.UsedLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, wp), sl));
							}
						}
					}
				}
			}
		}

		private void MarkAllMods(PIMNode nn, IRBasicAccessPath basep, IRSourceLocation sl)
		{
			HashSet<MemLocID> mlids = PIModel.LocationIDSForNode(nn);
			foreach(MemLocID ll in mlids)
			{
				if(!this.ReachableLocsAtSomePoint.Contains(ll))
					continue;

				IRType loctype = nn.LocationType;

				if(loctype is IRNumericType || loctype is IREnumType || loctype is IRPtrType || loctype is IRReferenceType)
					this.ModLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, basep), sl));
				else
				{
					if(basep.IsEmptyAccessPath)
					{
						foreach(IRBasicAccessPath pp in loctype.TypeDescription.AllTerminalAccessPaths)
							this.ModLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, pp), sl));
					}
					else
					{
						IRType storetype = basep.PathLast.FieldType;
						if(storetype is IRNumericType || storetype is IREnumType || storetype is IRPtrType || storetype is IRReferenceType)
							this.ModLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, basep), sl));
						else
						{
							foreach(IRBasicAccessPath pp in loctype.TypeDescription.AllTerminalAccessPaths)
							{
								IRBasicAccessPath wp = PProg.GetAccessPathExtensionPost_WPath(basep, pp);
								this.ModLocations.Add(new Tuple<IRType, MemLocWPath, IRSourceLocation>(loctype, MemLocWPath.MakeMemLocWithPath(ll, wp), sl));
							}
						}
					}
				}
			}
		}

		internal void AnalyzeCall(IRCallOp bc, List<ParamInfoCallSite> pci)
		{
			this.ResolveCallInfo(bc, pci);
		}

		internal void AnalyzeAlloc(IRAllocationOp bc, List<ParamInfoCallSite> pci)
		{
			if(bc.AllocType is IRContainerType && ((IRContainerType)bc.AllocType).IsArrayContainer)
				return;

			this.ResolveCallInfo(bc, pci);
		}

		internal void ResolveCallInfo(IRByteCode bc, List<ParamInfoCallSite> pci)
		{
			Dictionary<int, ProgramPointInfo> ppimap = CPInfoCTX.ProgramPointToPointInfoMap();
			ProgramPointInfo ppi = ppimap[bc.UseModLoc];
			
			List<IRInvokeIdentity> tiivl;
			if(bc is IRCallOp)
				tiivl = new List<IRInvokeIdentity>(((IRCallOp)bc).AnalysisResolvedCallTargets);
			else
				tiivl = new List<IRInvokeIdentity>() { ((IRAllocationOp)bc).ConsIdentity };

			foreach(IRInvokeIdentity iiv in tiivl)
			{
				IRBodyDef calleeb = PProg.MethodBodyTable.GetBodyForInvokeExactSigMatch(iiv);

				if(calleeb.IsBuiltin)
					this.AnalyzeBuiltin(iiv, calleeb.BuiltinSemanticName, ppi.PreOperationModel, bc.SourceLocationInfo);
				else
				{
					Dictionary<MemLocID, HashSet<MemLocID>> mlidd = new Dictionary<MemLocID, HashSet<MemLocID>>();

					//Lookup the info that relates the method call on the given line to the to callee methods and contexts that it may resolve to
					HashSet<CallerCalleeIDMapping> fccmapping = CPInfoCTX.CallToCalleeStateMaps[bc.UseModLoc];
					IEnumerable<CallerCalleeIDMapping> matches = fccmapping.Where((CallerCalleeIDMapping ccim) => ccim.CalleeInvokeIdentity == iiv && ccim.CallerContextID == CPInfoCTX.ContextID);
					foreach(CallerCalleeIDMapping ccmapping in matches)
					{
						foreach(KeyValuePair<MemLocID, HashSet<MemLocID>> mmkvp in ccmapping.CallerIDToCalleeIDMap)
						{
							foreach(MemLocID mml in mmkvp.Value)
							{
								if(!mlidd.ContainsKey(mml))
									mlidd.Add(mml, new HashSet<MemLocID>());
								mlidd[mml].Add(mmkvp.Key);
							}
						}
					}

					ParamInfoCallSite pics = new ParamInfoCallSite(iiv, bc.SourceLocationInfo, mlidd);
					pci.Add(pics);
				}
			}
		}
		
		internal void AnalyzeLoadFromLocal(IRLoadToEvalStackBasic bc, PIModel prem)
		{
			if(this.ParameterName != bc.LocalVar)
				return;

			PIMNode hn = prem.ResolveHomeForRoot(bc.LocalVar);
			this.MarkAllUses(hn, IRBasicAccessPath.EmptyAccessPath, bc.SourceLocationInfo);
		}

		internal void AnalyzeStoreToLocal(IRStoreFromEvalStackBasic bc, PIModel prem)
		{
			if(this.ParameterName != bc.LocalVar)
				return;

			PIMNode hn = prem.ResolveHomeForRoot(bc.LocalVar);
			this.MarkAllMods(hn, IRBasicAccessPath.EmptyAccessPath, bc.SourceLocationInfo);
		}

		internal void AnalyzeLoadFromGlobal(IRLoadToEvalStackBasic bc, PIModel prem)
		{
			if(this.ParameterName != bc.StaticField)
				return;

			PIMNode hn = prem.ResolveHomeForRoot(bc.StaticField);
			this.MarkAllUses(hn, IRBasicAccessPath.EmptyAccessPath, bc.SourceLocationInfo);
		}

		internal void AnalyzeStoreToGlobal(IRStoreFromEvalStackBasic bc, PIModel prem)
		{
			if(this.ParameterName != bc.StaticField)
				return;

			PIMNode hn = prem.ResolveHomeForRoot(bc.StaticField);
			this.MarkAllMods(hn, IRBasicAccessPath.EmptyAccessPath, bc.SourceLocationInfo);
		}

		internal void AnalyzeArrayLoad(IRLoadToEvalStackIndirect bc, PIModel prem)
		{
			IRMemberField sfield = ((IRContainerType)bc.ArrayLoadType).CardField;
			IRMemberField cfield = ((IRContainerType)bc.ArrayLoadType).ContentsField;
			
			PISNode lsn = prem.GetEvalStackNodeAtPos(1);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(sfield), bc.SourceLocationInfo);
				this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(cfield), bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeArrayStore(IRStoreFromEvalStackIndirect bc, PIModel prem)
		{
			IRMemberField sfield = ((IRContainerType)bc.ArrayStoreType).CardField;
			IRMemberField cfield = ((IRContainerType)bc.ArrayStoreType).ContentsField;
			
			PISNode lsn = prem.GetEvalStackNodeAtPos(2);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(sfield), bc.SourceLocationInfo);
				this.MarkAllMods(nn, PProg.GetAccessPathForSingleField(cfield), bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeArrayLength(IRByteCode bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				IRContainerType cc = (IRContainerType)nn.LocationType;

				this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(cc.CardField), bc.SourceLocationInfo);
			}
		}
		
		internal void AnalyzeIndirectRead(IRByteCode bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, ee.OffsetInTarget, bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeIndirectWrite(IRByteCode bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(1);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllMods(nn, ee.OffsetInTarget, bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeLoadMemberField(IRLoadToEvalStackIndirect bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(bc.LoadField), bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeStoreMemberField(IRStoreFromEvalStackIndirect bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(1);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllMods(nn, PProg.GetAccessPathForSingleField(bc.WriteField), bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeIndirectInitialize(IRStoreFromEvalStackIndirect bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllMods(nn, ee.OffsetInTarget, bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeUnbox(IREvalStackTypeOp bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				IRBoxedType bt = (IRBoxedType)nn.LocationType;
				this.MarkAllMods(nn, PProg.GetAccessPathForSingleField(bt.BoxedValueField), bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeCast(IRByteCode bc, PIModel prem)
		{
			IRMemberField rttif = PProg.TypeTable.RootObjectRTTIField;
			IRBasicAccessPath rttibap = PProg.GetAccessPathForSingleField(rttif);

			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, rttibap, bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeIsInst(IRByteCode bc, PIModel prem)
		{
			IRMemberField rttif = PProg.TypeTable.RootObjectRTTIField;
			IRBasicAccessPath rttibap = PProg.GetAccessPathForSingleField(rttif);

			PISNode lsn = prem.GetEvalStackNodeAtPos(0);
			foreach(PIMEdge ee in lsn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkAllUses(nn, rttibap, bc.SourceLocationInfo);
			}
		}

		internal void AnalyzeConstrain(IRType constrinto, int pos, IRByteCode bc, PIModel prem)
		{
			PISNode lsn = prem.GetEvalStackNodeAtPos(pos);

			if(constrinto is IRReferenceType)
			{ ;}
			else
			{
				Contract.Assert(constrinto is IRPtrType);

				IRType atype = ((IRPtrType)constrinto).PtrTargetType;
				foreach(PIMEdge ee in lsn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkAllUses(nn, ee.OffsetInTarget, bc.SourceLocationInfo);
				}
			}
		}

		////////////////////////////////////////////////////////////////////////////
		//Handle builtin methods

		private void MarkFieldUseBI(PIMNode nn, IRMemberField f, IRSourceLocation sl)
		{ this.MarkAllUses(nn, PProg.GetAccessPathForSingleField(f), sl); }

		private void MarkFieldModBI(PIMNode nn, IRMemberField f, IRSourceLocation sl)
		{ this.MarkAllMods(nn, PProg.GetAccessPathForSingleField(f), sl); }

		private void MarkStringValueReadsBI(PISNode sn, PIModel prem, IRSourceLocation sl)
		{
			IRMemberField slf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("slen");
			IRBasicAccessPath slfp = PProg.GetAccessPathForSingleField(slf);
			IRMemberField svf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("sval");
			IRBasicAccessPath svfp = PProg.GetAccessPathForSingleField(svf);

			foreach(PIMEdge te in sn.Targets)
			{
				PIMNode nn = prem.Nodes[te.TargetAddress];
				this.MarkAllUses(nn, slfp, sl);
				this.MarkAllUses(nn, svfp, sl);
			}
		}

		private void MarkStringValueReadsBI(PIMNode nn, IRSourceLocation sl)
		{
			IRMemberField slf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("slen");
			IRBasicAccessPath slfp = PProg.GetAccessPathForSingleField(slf);
			IRMemberField svf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("sval");
			IRBasicAccessPath svfp = PProg.GetAccessPathForSingleField(svf);

			this.MarkAllUses(nn, slfp, sl);
			this.MarkAllUses(nn, svfp, sl);
		}

		private void MarkListCCUsed(PISNode sn, IRContainerType rcvrtype, PIModel prem, IRSourceLocation sl)
		{
			foreach(PIMEdge ee in sn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkFieldUseBI(nn, ((IRContainerType)rcvrtype).CardField, sl);
				this.MarkFieldUseBI(nn, ((IRContainerType)rcvrtype).ContentsField, sl);
			}
		}

		private void MarkListCCMod(PISNode sn, IRContainerType rcvrtype, PIModel prem, IRSourceLocation sl)
		{
			foreach(PIMEdge ee in sn.Targets)
			{
				PIMNode nn = prem.Nodes[ee.TargetAddress];
				this.MarkFieldModBI(nn, ((IRContainerType)rcvrtype).CardField, sl);
				this.MarkFieldModBI(nn, ((IRContainerType)rcvrtype).ContentsField, sl);
			}
		}

		/// <summary>
		/// Write to the global filesytem value.
		/// </summary>
		private void HavocExternalStateBI(PIModel prem, IRSourceLocation sl)
		{
			IRClassType cty = (IRClassType)PProg.TypeTable.LookupTypeForName("System.ExternalState");
			IRStaticField sfd = PProg.NameTable.LookupStaticField(cty, "fsstate");

			PIMNode hn = prem.ResolveHomeForRoot(sfd);
			this.MarkAllUses(hn, IRBasicAccessPath.EmptyAccessPath, sl);
			this.MarkAllMods(hn, IRBasicAccessPath.EmptyAccessPath, sl);
		}

		/// <summary>
		/// A big switch of what to do for builtins
		/// </summary>
		internal void AnalyzeBuiltin(IRInvokeIdentity binv, string mns, PIModel prem, IRSourceLocation sl)
		{
			int argc = (binv.Sig.IsVirtualInvoke ? (binv.Sig.InvokeSig.Count + 1) : binv.Sig.InvokeSig.Count);
			int baseoffset = (argc - 1);

			IRType rcvrtype = binv.DefInClass;

			if(mns.Equals("object_init") || mns.Equals("list_alloc_default") || mns.Equals("hashset_init") || mns.Equals("init_keyvalpair") || mns.Equals("dictionary_init") || mns.Equals("stringbuilder_alloc"))
			{ ;}
			else if(mns.Equals("nop"))
			{ ;}
			else if(mns.Equals("object_equals") || mns.Equals("object_equals_staticbyref"))
			{ ;}
			else if(mns.Equals("string_from_chars_rng"))
			{
				PISNode ca = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				foreach(PIMEdge te in ca.Targets)
				{
					PIMNode nn = prem.Nodes[te.TargetAddress];
					IRContainerType catype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, catype.CardField, sl);
					this.MarkFieldUseBI(nn, catype.ContentsField, sl);
				}
			}
			else if(mns.Equals("filestream_init"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				this.MarkStringValueReadsBI(sn, prem, sl);
				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("object_hashcode") || mns.Equals("object_hashcode_static"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge te in sn.Targets)
				{
					PIMNode tn = prem.Nodes[te.TargetAddress];
					this.MarkFieldUseBI(tn, PProg.TypeTable.RootObjectRTTIField, sl);
				}
			}
			else if(mns.Equals("memberwise_copy"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge te in sn.Targets)
				{
					PIMNode tn = prem.Nodes[te.TargetAddress];
					this.MarkAllUses(tn, IRBasicAccessPath.EmptyAccessPath, sl);
				}
				
			}
			else if(mns.Equals("internal_string_compare"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset - 2), prem, sl);
			}
			else if(mns.Equals("ceiling_double") || mns.Equals("floor_double") || mns.Equals("log_double") || mns.Equals("sqrt_double"))
			{ ;}
			else if(mns.Equals("pow_double") || mns.Equals("sin_double") || mns.Equals("cos_double") || mns.Equals("tan_double"))
			{ ;}
			else if(mns.Equals("exit_program"))
			{ ;}
			else if(mns.Equals("concat_string_array"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					IRContainerType ctype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, ctype.CardField, sl);
					this.MarkFieldUseBI(nn, ctype.ContentsField, sl);

					foreach(PIMEdge te in nn.OutEdges)
					{
						PIMNode tn = prem.Nodes[te.TargetAddress];
						this.MarkStringValueReadsBI(tn, sl);
					}
				}
			}
			else if(mns.Equals("get_string_length"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				IRMemberField slf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("slen");
				IRBasicAccessPath slfp = PProg.GetAccessPathForSingleField(slf);

				foreach(PIMEdge te in sn.Targets)
				{
					PIMNode nn = prem.Nodes[te.TargetAddress];
					this.MarkAllUses(nn, slfp, sl);
				}
			}
			else if(mns.Equals("get_string_char"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				IRMemberField svf = PProg.TypeTable.StringObjectType.TypeDescription.GetFieldWithNameDefIn("sval");
				IRBasicAccessPath svfp = PProg.GetAccessPathForSingleField(svf);

				foreach(PIMEdge te in sn.Targets)
				{
					PIMNode nn = prem.Nodes[te.TargetAddress];
					this.MarkAllUses(nn, svfp, sl);
				}
			}
			else if(mns.Equals("internal_string_formatbuild"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);

				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					IRContainerType ctype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, ctype.CardField, sl);
					this.MarkFieldUseBI(nn, ctype.ContentsField, sl);

					foreach(PIMEdge te in nn.OutEdges)
					{
						PIMNode tn = prem.Nodes[te.TargetAddress];
						this.MarkStringValueReadsBI(tn, sl);
					}
				}
			}
			else if(mns.Equals("bool_get_truth"))
			{ ;}
			else if(mns.Equals("char_is_whitepace"))
			{ ;}
			else if(mns.Equals("parse_as_integral") || mns.Equals("parse_as_usignintegral") || mns.Equals("parse_as_floatingpoint"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);
			}
			else if(mns.Equals("format_integral_as_string") || mns.Equals("format_usignintegral_as_string") || mns.Equals("format_floatingpoint_as_string"))
			{ ;}
			else if(mns.Equals("get_string_hashcode"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);
			}
			else if(mns.Equals("string_replace") || mns.Equals("string_indexof_string"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset - 1), prem, sl);
			}
			else if(mns.Equals("string_split"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);

				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					IRContainerType ctype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, ctype.CardField, sl);
					this.MarkFieldUseBI(nn, ctype.ContentsField, sl);
				}
			}
			else if(mns.Equals("string_trim"))
			{
				this.MarkStringValueReadsBI(prem.GetEvalStackNodeAtPos(baseoffset), prem, sl);
			}
			else if(mns.Equals("havoc_externalstate"))
			{
				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("array_sort_on"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("list_add"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_clear"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_insert_index"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_make_space"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_removeat"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_removeflags"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);

				PISNode sna = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				foreach(PIMEdge ee in sna.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					IRContainerType actype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, actype.CardField, sl);
					this.MarkFieldUseBI(nn, actype.ContentsField, sl);
				}
			}
			else if(mns.Equals("list_reverse"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_sort_on"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);

				PISNode sna = prem.GetEvalStackNodeAtPos(baseoffset - 1);
				foreach(PIMEdge ee in sna.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					IRContainerType actype = (IRContainerType)nn.LocationType;
					this.MarkFieldUseBI(nn, actype.CardField, sl);
					this.MarkFieldUseBI(nn, actype.ContentsField, sl);
				}
			}
			else if(mns.Equals("list_getcount") || mns.Equals("hashset_getcount") || mns.Equals("dictionary_getcount"))
			{
				PISNode sna = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge ee in sna.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkFieldUseBI(nn, ((IRContainerType)rcvrtype).CardField, sl);
				}
			}
			else if(mns.Equals("list_getitem"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("list_setitem"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				this.MarkListCCUsed(sn, (IRContainerType)rcvrtype, prem, sl);
				this.MarkListCCMod(sn, (IRContainerType)rcvrtype, prem, sl);
			}
			else if(mns.Equals("hashset_gethvalid"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashset_getvalue"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashset_resizeasneeded"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashset_clear"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashset_adddirect"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashet_removeatdirect"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("hashet_removeatflags"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("get_key"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("get_value"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_gethvalid"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_getvalue"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_resizeasneeded"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_clear"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_adddirect"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("dictionary_removeatdirect"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("valuetype_equals"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkAllUses(nn, IRBasicAccessPath.EmptyAccessPath, sl);
				}
			}
			else if(mns.Equals("valuetype_hashcode"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkAllUses(nn, IRBasicAccessPath.EmptyAccessPath, sl);
				}
			}
			else if(mns.Equals("valuetype_equals_static"))
			{ ;}
			else if(mns.Equals("valuetype_hashcode_static"))
			{ ;}
			else if(mns.Equals("valuetype_tostring"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkAllUses(nn, IRBasicAccessPath.EmptyAccessPath, sl);
				}
			}
			else if(mns.Equals("enum_compareto"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("datetime_to_universal"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("datetime_to_local"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("datetime_now"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("datetime_tofileutc"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("datetime_internalkind"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("filestream_close"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("filestream_read"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("filestream_seek"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("filestream_write"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("filestream_length"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("stdin_init"))
			{
				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("stdout_init"))
			{
				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("stdin_readchar"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				IRMemberField statef = rcvrtype.TypeDescription.GetFieldWithNameDefIn("state");

				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkFieldUseBI(nn, statef, sl);
				}

				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("stdout_writechar"))
			{
				PISNode sn = prem.GetEvalStackNodeAtPos(baseoffset);
				IRMemberField statef = rcvrtype.TypeDescription.GetFieldWithNameDefIn("state");

				foreach(PIMEdge ee in sn.Targets)
				{
					PIMNode nn = prem.Nodes[ee.TargetAddress];
					this.MarkFieldUseBI(nn, statef, sl);
				}

				this.HavocExternalStateBI(prem, sl);
			}
			else if(mns.Equals("file_copy"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("file_delete"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("file_exists"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("file_move"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("fsaccess_getinfo"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("fsaccess_setinfo"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_create"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_delete"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_getfilesordirs"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_exists"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_current"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("directory_move"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("path_normalize"))
			{
				throw new NotImplementedException();
			}
			else if(mns.Equals("binaryconv_fromdouble") || mns.Equals("binaryconv_fromfloat"))
			{ ;}
			else if(mns.Equals("binaryconv_todouble") || mns.Equals("binaryconv_tofloat"))
			{ ;}
			else if(mns.Equals("monitor_exit") || mns.Equals("monitor_enter"))
			{ ;}
			else
				DebugReport.ReportError("Unknown Builtin Method: " + mns);
		}
	}
}
